A, B:es_realizer{i:l}, P:(ES{i}Prop{i'}).
R-Feasible{i:l}(A)  B ||-{i} es.P(es)  R-compat{i:l}(A; B)  A  B ||-{i} es.P(es) 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s), t  T, x. t(x), True, P & Q
Lemmas	R-and-rule, true wf, R-compat wf, R-realizes wf, event system wf, R-Feasible wf, es realizer wf, R-true-rule, R-implies-rule, Rplus wf